i, a:Id, T:Type, ds:x:Id fp Type, P:(State(ds)TProp).
@i (with ds: ds action a:T precondition a(v) is P s v)  Dsys 

latex

Definitions	Dsys, @i (with ds: ds action a:T precondition a(v) is P s v), if b t else f fi, eqof(d), IdDeq, MsgA, (with ds: ds action a:T precondition a(v) is P s v), , State(ds), Prop, a:A fp B(a), x:A. B(x), x. t(x), t  T, Id
Lemmas	Id wf, fpf wf, ma-state wf, ma-empty wf, ma-single-pre wf, msga wf, id-deq wf, eqof wf, ifthenelse wf